Some questions about using ekl or fol in cs206

1. Should we prove programs for a subset of maclisp or
use a special lisp all of whose programs are transformable
to first order sentences in the formalism we intend to use.

If we stick to maclisp, then we may want to accept only
those programs that generate only T and NIL as truth
values including those used in conditional expressions,
and we will want to use conditional expressions with
precisely two element lists as conditions.

2. The job includes the following:

	a. A program that checks defuns to see that they
meet specifications for translation to sentences and
then translates them accordingly.  If we want to we can
make it generate sentences corresponding
to modified programs that look at all their arguments,
so that the proofs apply to call-by-value lisp.

	b. A collection of axioms suitable for proving
facts about subsequently defined lisp functions.

	c. Suitable collections of canned simplification
rules that will permit symbolic evaluation.

	d. A collection of worked examples that use
the precise facilities provided.

3. To what extent do we use both logical and data
domain conditional expressions (d.d.c.e).  I favor using both
and transforming programs that use d.d.c.e.s into
sentences using logical c.e.s as soon as the required
termination theorems have been proved.  Where the
form permits initial use of logical c.e.s, perhaps
the defun transformer produce a sentence with this
property.

4. Shall we preserve the separate domains of pairs
and atoms.  I find it a pain and prefer to use
conditional expressions using general S-expression
variables.  To do this in a fully flexible way
requires a replacement rule that allows proving

	if p then a else b = if p then a' else b

from p  a=a'

and proving

	if p then a else b = if p then a else b'

from

	p  b=b'.